package com.googlecode.kipler.satisfiability.completion.branching;

import com.googlecode.kipler.container.dl.DependencySet;
import com.googlecode.kipler.container.dl.World;
import com.googlecode.kipler.container.dl.WorldConstraintSystem;
import com.googlecode.kipler.satisfiability.reasoner.UnsatisfiableException;

/**
 * 
 * @author İnanç Seylan
 * 
 * This stack is used to simulate the tree characteristic of the tableau
 * algorithm. Each application of a branching rule generates a new world
 * constraint system. We have to consider each of these world constraint systems
 * until one is found that is complete and satisfiable. This stack allows us to
 * visit these world constraint systems as if we're traversing a tree.
 * 
 */
public abstract class BranchingPoint {
	private WorldConstraintSystem wcs;

	private World world;

	private DependencySet lastDependencySet = new DependencySet();

	private BranchingPoint previous;

	/**
	 * @return the wcs
	 */
	public WorldConstraintSystem getWcs() {
		return wcs;
	}

	/**
	 * @param wcs
	 *            the wcs to set
	 */
	public void setWcs(WorldConstraintSystem wcs) {
		this.wcs = wcs;
	}

	/**
	 * @return the world
	 */
	public World getWorld() {
		return world;
	}

	/**
	 * @param world
	 *            the world to set
	 */
	public void setWorld(World world) {
		this.world = world;
	}

	public void setLastBranchDependencies(DependencySet dependencies) {
		lastDependencySet = dependencies;
	}

	public DependencySet getLastBranchDependencies() {
		return lastDependencySet;
	}

	public void setNextBranchingPoint(BranchingPoint bp) {
		bp.previous = this;
	}

	public boolean hasPreviousBranchingPoint() {
		return previous != null;
	}

	public BranchingPoint previousBranchingPoint() {
		backtrack();
		return previous;
	}

	public abstract boolean isBranchingPossible();

	public abstract WorldConstraintSystem nextBranch()
			throws UnsatisfiableException;

	public abstract void backtrack();

}
